$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it ll}$:($T$ List List), $x$:$T$.
\\[0ex]($x$ $\in$ l{-}union{-}list(${\it eq}$; ${\it ll}$)) $\Leftarrow\!\Rightarrow$ ($\exists$$l$:$T$ List. (($l$ $\in$ ${\it ll}$) $\wedge$ ($x$ $\in$ $l$)))